/*
 * ParamArray.java
 * 
 * Copyright 2004 Christoph Csallner and Yannis Smaragdakis.
 */
package edu.gatech.cc.cnc.params;

import edu.gatech.cc.cnc.Main;
import edu.gatech.cc.cnc.sym;
import edu.gatech.cc.cnc.plans.stmt.ArrayCreatingBlockStatementSequence;
import edu.gatech.cc.jcrasher.plans.expr.Expression;
import edu.gatech.cc.jcrasher.plans.expr.Variable;
import edu.gatech.cc.jcrasher.plans.stmt.BlockStatement;
import edu.gatech.cc.jcrasher.plans.stmt.LocalVariableDeclarationStatement;

/**
 * elems maps key i to the i-th array element.
 * elems: String "0" --> Param p
 * elems: ParamIntegral k --> Param p, params: String kName --> ParamIntegral k. 
 *  
 * @author csallner@gatech.edu (Christoph Csallner)
 */
public class ParamArray<T> extends ParamRefType<T> {
	/* Insert (fieldName, fieldWrapper) into elems 
	 * on parsing a constraint on fieldName. */
	
	/* array length is an int in Java. */
	protected ParamInt arrayLength = 
		new ParamInt(0, ParamInt.getDomain().getMax(), "<length>");
	
	
	/**
	 * Constructor
	 */
	public ParamArray(Class<T> wrappedType, String name) {
		super(name);
		setType(wrappedType);
		getEq().addTuple(this);  //register in equivalence relation.
	}

	
	/**
	 * TODO resolve def-use conflict:
	 * a) int-solver determines index nameVar
	 * b) identity propagation to n-th element as precondition to int-solver.s
	 */
	public void addElem(ParamIntegral<?> nameVar, Param<?> param) {
		/* do not register name, as it is not resolved yet. */
		elems.put(nameVar, param);
	}
	

	/**
	 * @return int variable representing the length of this array.
	 */
	public ParamInt getArrayLength() {
		return arrayLength;
	}


	/**
	 * @return Param at position key, or null.
	 */
	public Param<?> getElem(ParamIntegral<?> key) {
		assert (key!=null);
		return elems.get(key);  
	}		
	
	/** 
	 * @return whether (i=j --> a[i]=a[j]) holds.
	 */
	public boolean isFunctional() {
		if (getArrayLength().getValue() > Main.MAX_ARRAY_LENGTH) {
			return true;  //do not check large arrays---too expensive.
		}
		
		/* Assemble resulting array and check property. */
		Param[] array = new Param[getArrayLength().getValue()];
		for (Object keyO: getElemKeys()) {
			int key = -1;
			Param<?> val = null;
			if (keyO instanceof String) {
				key = Integer.parseInt((String)keyO);
				val = getElemValue((String)keyO);
			}
			else {
				assert (keyO instanceof ParamIntegral);
				key = ((ParamIntegral)keyO).getValue();
				val = getElem((ParamIntegral)keyO);
			}
			if (key<0 || key>=array.length) {return false;} //not even an array.
			if (array[key]!=null) {  //check whether old val == val.				
				if (val instanceof ParamIntegral) {
					/* int-solver decides */
					if (((ParamIntegral)array[key]).getValue() != ((ParamIntegral<?>)val).getValue()) {return false;}
				}				
				if ((val instanceof ParamRefType) && !getEq().getEqualValues((ParamRefType<?>)val).contains(array[key])) {
					/* constraint (a[b=c] != a[c]) */
					if (((ParamRefType<?>)val).neqContains((ParamRefType<?>)array[key])) {return false;}
				}
				//TODO more complex static analysis to revoke unsound array.
			}
			array[key]=val;
		}
		return true;
	}
	
	
	
	/**
	 * @returns whether (i=j --> a[i]=a[j]) holds for all array parameters.
	 */
	public static boolean areArraysFunctional() {
		for (Param<?> p: getEq().getKeys()) {
			if (p instanceof ParamArray) {
				if (((ParamArray<?>)p).isFunctional() == false) 
					return false;
			}
		}
		return true;		
	}	


	@Override
	public void constrain(int relation2, Param<?> rhs) {
		super.constrain(relation2, rhs);
		
		/* make sure array lengths are equal.
		 * All other identities are given by ESC, as ESC reports constraints
		 * only on a single representative of a equivalence class. */
		if (relation2 == sym.EQ) {
			arrayLength.constrain(sym.EQ, ((ParamArray<?>)rhs).arrayLength);
		}			
	}	
	
	
	/* Precondition: 
	 * + The int solver has generated a solution--- 
	 *   this method retrieves part of this solution.
	 * + isFunctional() established for this solution---
	 *   otherwise this solution might not satisfy the counterexample.
	 * @see edu.gatech.cc.jcrasher.testall.escjava.Param#getPlan()
	 */
	protected BlockStatement<? extends T> planFromElems(Variable<T> id) {
		if (getArrayLength().getValue() > Main.MAX_ARRAY_LENGTH) {
      Expression<? extends T> value = JCrasherPlanner.instance().getRandom(getType(), testeeType);  //do not plan for huge arrays. 
			return new LocalVariableDeclarationStatement(nextID(getType()), value); 
		}
		
		/* Small array, so do actual planning. */
		BlockStatement<?>[] elemPlans = new BlockStatement[getArrayLength().getValue()];
		
		/* Fill with default values. */
		for (int i=0; i<elemPlans.length; i++) {
      Expression<?> value = 
        JCrasherPlanner.instance().getRandom(getType().getComponentType(), testeeType);
			elemPlans[i] = new LocalVariableDeclarationStatement(
            nextID(getType().getComponentType()),
            value); 
		}
		
		/* Overwrite defaults with solutions of constraint system. */
		for (Object keyO: getElemKeys()) {
			int key = -1;
			Param<?> param = null;
			if (keyO instanceof String) {
				key = Integer.parseInt((String)keyO);
				param = getElemValue((String) keyO);
			}
			if (keyO instanceof ParamIntegral) {
				key = ((ParamIntegral)keyO).getValue();
				param = getElem((ParamIntegral) keyO);
			}
			elemPlans[key] = param.getPlan(); 
		}
		
		return new ArrayCreatingBlockStatementSequence(testeeType, block, id, elemPlans);
	}
}
